package org.adoxx.pn.output;

import java.util.ArrayList;

import org.adoxx.pn.PetriNet;
import org.adoxx.pn.PetriNet.PL;
import org.adoxx.pn.PetriNet.TR;

public class ExporterEldarica {

    
    public static String exportTo_EldaricaP(PetriNet pn) throws Exception{
        if(pn.isEmpty())
            throw new Exception("ERROR: The provided petri net is empty");
        
        String ret = "net {\""+pn.getName()+"\"}\n";
        
        for(TR tr:pn.getTransitionList_safe()){
            ret += "\ntr " + tr.name + " [] ";
            for(PL pl:tr.previousList)
                ret += pl.name + " ";
            ret += "->";
            for(PL pl:tr.nextList)
                ret += " " + pl.name;
        }
        
        ret += "\n";
        for(PL pl:pn.getStartList_safe())
            ret += "\npl " + pl.name + " (" + pl.numToken + ")";
        
        return ret;
    }
    
    public static String exportTo_EldaricaP_property_EndReachability(PetriNet pn) throws Exception{
        if(pn.isEmpty())
            throw new Exception("ERROR: The provided petri net is empty");
        
        String finalConfig = "";
        for(PL pl:pn.getEndList_safe())
            finalConfig += "\nfinal " + pl.name + " (1)";
        return finalConfig;
    }
    
    public static String exportTo_EldaricaP_property_DeadlockPresence(PetriNet pn) throws Exception{
        //C'e' deadlock se tutte le transizioni non sono attivabili e c'e' almeno un place non finale che contiene uno o piu token
        
        if(pn.isEmpty())
            throw new Exception("ERROR: The provided petri net is empty");
        
        String finalConfig = "finalConfiguration (";
        
        for(TR tr:pn.getTransitionList_safe()){
            finalConfig += "\n (";
            for(PL pl:tr.previousList)
                finalConfig += pl.name + " = 0 | ";
            finalConfig = finalConfig.substring(0, finalConfig.length()-2) + ")&";
        }
        
        finalConfig += "\n\n (";
        ArrayList<PL> endList = pn.getEndList_safe();
        for(PL pl:pn.getPlaceList_safe())
            if(!endList.contains(pl))
                if(!pl.excludeFromDeadlockCheck)
                    finalConfig += pl.name + " > 0 | ";
        if(finalConfig.endsWith("| "))
            finalConfig = finalConfig.substring(0, finalConfig.length()-2) + ")\n)";
        else
            finalConfig = finalConfig.substring(0, finalConfig.length()-5) + ")";
        
        return finalConfig;
    }
}
